<html>
<head><meta charset="utf-8"><title>Chalk book modeling orphan check · wg-traits · Zulip Chat Archive</title></head>
<h2>Stream: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/index.html">wg-traits</a></h2>
<h3>Topic: <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html">Chalk book modeling orphan check</a></h3>

<hr>

<base href="https://rust-lang.zulipchat.com">

<head><link href="https://rust-lang.github.io/zulip_archive/style.css" rel="stylesheet"></head>

<a name="235581622"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235581622" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235581622">(Apr 21 2021 at 21:06)</a>:</h4>
<p><a href="https://rust-lang.github.io/chalk/book/clauses/coherence.html#modeling-the-orphan-check">https://rust-lang.github.io/chalk/book/clauses/coherence.html#modeling-the-orphan-check</a></p>



<a name="235581683"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235581683" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235581683">(Apr 21 2021 at 21:06)</a>:</h4>
<p>where it says ...</p>



<a name="235581689"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235581689" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235581689">(Apr 21 2021 at 21:06)</a>:</h4>
<blockquote>
<p>If Trait is local to the current crate, we generate: <code>forall&lt;Self, P1…Pn&gt; { LocalImplAllowed(Self: Trait&lt;P1...Pn&gt;) }</code> This models that any impls are allowed if the trait is local to the current crate.</p>
</blockquote>



<a name="235581713"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235581713" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235581713">(Apr 21 2021 at 21:07)</a>:</h4>
<p>I think that should be ...</p>



<a name="235581822"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235581822" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235581822">(Apr 21 2021 at 21:07)</a>:</h4>
<blockquote>
<p>If Trait is local to the current crate, we generate: <code>forall&lt;Self, P1…Pn&gt; { LocalImplAllowed(Self: Trait&lt;P1...Pn&gt;)  :- IsLocal(Trait&lt;P1...Pn&gt;)}</code> This models that any impls are allowed if the trait is local to the current crate.</p>
</blockquote>



<a name="235581890"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235581890" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235581890">(Apr 21 2021 at 21:07)</a>:</h4>
<p>right?</p>



<a name="235582647"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235582647" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235582647">(Apr 21 2021 at 21:11)</a>:</h4>
<p>So, I'd have to look at the actual clauses that we generate. Your <code>:- IsLocal(...)</code> I think is logically correct</p>



<a name="235582808"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235582808" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235582808">(Apr 21 2021 at 21:12)</a>:</h4>
<p>But we don't generate those conditions in some cases where we know them ahead of time</p>



<a name="235582874"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235582874" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235582874">(Apr 21 2021 at 21:12)</a>:</h4>
<p>like the previous statement is not even actually a clause :) the <code>:-</code> is missing</p>



<a name="235582971"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235582971" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235582971">(Apr 21 2021 at 21:12)</a>:</h4>
<p>if you want I can provide a PR with that change so we can discuss there or merge if you agree that's the right change</p>



<a name="235583134"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235583134" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235583134">(Apr 21 2021 at 21:13)</a>:</h4>
<p>let me just quickly go look at the code</p>



<a name="235583545"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235583545" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235583545">(Apr 21 2021 at 21:15)</a>:</h4>
<div class="codehilite" data-code-language="Diff"><pre><span></span><code><span class="gh">diff --git a/book/src/clauses/coherence.md b/book/src/clauses/coherence.md</span>
<span class="gh">index 190dac99..a8ddfde5 100644</span>
<span class="gd">--- a/book/src/clauses/coherence.md</span>
<span class="gi">+++ b/book/src/clauses/coherence.md</span>
<span class="gu">@@ -90,7 +90,7 @@ Here’s how the lowering rules would look:</span>
 For each trait `Trait`,

 - If `Trait` is local to the current crate, we generate:
<span class="gd">-    `forall&lt;Self, P1…Pn&gt; { LocalImplAllowed(Self: Trait&lt;P1...Pn&gt;) }`</span>
<span class="gi">+    `forall&lt;Self, P1…Pn&gt; { LocalImplAllowed(Self: Trait&lt;P1...Pn&gt;) :- IsLocal(Trait&lt;P1...Pn&gt;) }`</span>
     This models that any impls are allowed if the trait is local to the current crate.
 - If `Trait` is upstream to the current crate, we need a rule which models the additional conditions on which impls are allowed:
 ```ignore
</code></pre></div>



<a name="235583814"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235583814" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235583814">(Apr 21 2021 at 21:16)</a>:</h4>
<p><span class="user-mention silent" data-user-id="232957">Jack Huey</span> <a href="#narrow/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check/near/235583134">said</a>:</p>
<blockquote>
<p>let me just quickly go look at the code</p>
</blockquote>
<p>point out to the code you are looking at :), may be interesting to see</p>



<a name="235583852"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235583852" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235583852">(Apr 21 2021 at 21:16)</a>:</h4>
<p><a href="https://github.com/rust-lang/chalk/blob/d0d8fbe20dd17d5edce38e40b0551df4b065f996/chalk-solve/src/clauses/program_clauses.rs#L684">https://github.com/rust-lang/chalk/blob/d0d8fbe20dd17d5edce38e40b0551df4b065f996/chalk-solve/src/clauses/program_clauses.rs#L684</a></p>



<a name="235583869"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235583869" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235583869">(Apr 21 2021 at 21:16)</a>:</h4>
<p>Trying to figure out if that's the relevant code</p>



<a name="235583972"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235583972" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235583972">(Apr 21 2021 at 21:17)</a>:</h4>
<p>So, line 681</p>



<a name="235584053"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235584053" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235584053">(Apr 21 2021 at 21:18)</a>:</h4>
<p>Because of the <code>!self.flags.upstream</code> check, we don't <em>need</em> the <code>IsLocal(...)</code> condition</p>



<a name="235584070"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235584070" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235584070">(Apr 21 2021 at 21:18)</a>:</h4>
<p>Because that <em>is</em> the condition itself</p>



<a name="235584112"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235584112" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235584112">(Apr 21 2021 at 21:18)</a>:</h4>
<p>Also, we don't <em>have</em> an <code>IsLocal(Trait)</code> goal</p>



<a name="235584136"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235584136" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235584136">(Apr 21 2021 at 21:19)</a>:</h4>
<p>Relevant goal for <code>Ty</code>: <a href="https://github.com/rust-lang/chalk/blob/d0d8fbe20dd17d5edce38e40b0551df4b065f996/chalk-ir/src/lib.rs#L1856">https://github.com/rust-lang/chalk/blob/d0d8fbe20dd17d5edce38e40b0551df4b065f996/chalk-ir/src/lib.rs#L1856</a></p>



<a name="235584283"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235584283" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235584283">(Apr 21 2021 at 21:20)</a>:</h4>
<p>I see</p>



<a name="235584307"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235584307" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235584307">(Apr 21 2021 at 21:20)</a>:</h4>
<p><a href="https://github.com/rust-lang/chalk/blob/d0d8fbe20dd17d5edce38e40b0551df4b065f996/chalk-solve/src/clauses/program_clauses.rs#L511-L514">https://github.com/rust-lang/chalk/blob/d0d8fbe20dd17d5edce38e40b0551df4b065f996/chalk-solve/src/clauses/program_clauses.rs#L511-L514</a></p>



<a name="235584347"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235584347" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235584347">(Apr 21 2021 at 21:20)</a>:</h4>
<p>so that thing per se is considered a fact, I guess?</p>



<a name="235584470"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235584470" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235584470">(Apr 21 2021 at 21:21)</a>:</h4>
<p>Well, if we check if <code>Trait</code> is not upstream, then we can take <code>IsLocal(Trait&lt;P1...Pn&gt;) }</code> as fact</p>



<a name="235584555"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235584555" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235584555">(Apr 21 2021 at 21:22)</a>:</h4>
<p>We do something similar with some other wf/coherence related things. Blanking on which ones</p>



<a name="235584637"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235584637" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235584637">(Apr 21 2021 at 21:22)</a>:</h4>
<p>I was expecting something like <code>LocalImplAllowed(Self: Trait&lt;P1...Pn&gt;)</code> to not be considered as a goal and as a fact at the same time</p>



<a name="235584647"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235584647" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235584647">(Apr 21 2021 at 21:22)</a>:</h4>
<p>unsure if I'm explaining myself correctly</p>



<a name="235584698"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235584698" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235584698">(Apr 21 2021 at 21:22)</a>:</h4>
<p>but if you see <code>LocalImplAllowed(Self: Trait&lt;P1...Pn&gt;)</code> in some cases is at the left side of the <code>:-</code> and in some cases like this is just fact</p>



<a name="235584706"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235584706" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235584706">(Apr 21 2021 at 21:23)</a>:</h4>
<p>I wasn't sure if that was "valid"</p>



<a name="235584748"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235584748" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235584748">(Apr 21 2021 at 21:23)</a>:</h4>
<p>See <a href="https://github.com/rust-lang/chalk/pull/566">https://github.com/rust-lang/chalk/pull/566</a></p>



<a name="235584782"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235584782" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235584782">(Apr 21 2021 at 21:23)</a>:</h4>
<p>I'm not sure I follow</p>



<a name="235584876"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235584876" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235584876">(Apr 21 2021 at 21:24)</a>:</h4>
<p>So, <code>wf.rs</code> tries to solve <code>LocalImplAllowed(Self: Trait&lt;P1...Pn&gt;)</code></p>



<a name="235584910"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235584910" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235584910">(Apr 21 2021 at 21:24)</a>:</h4>
<p>And to solve that, <code>program_clauses</code> pushes relevant clauses</p>



<a name="235585064"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235585064" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235585064">(Apr 21 2021 at 21:25)</a>:</h4>
<p>But either that is <em>just true</em> (if the trait is local), or it's conditionally true</p>



<a name="235585192"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235585192" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235585192">(Apr 21 2021 at 21:26)</a>:</h4>
<p>If we had a <code>IsLocal(Trait)</code> goal, then <code>program_clauses</code> could add <em>both</em></p>



<a name="235585260"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235585260" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235585260">(Apr 21 2021 at 21:27)</a>:</h4>
<p>But <code>IsLocal(Trait)</code> would essentially be solvable if <code>Trait</code> is not upstream</p>



<a name="235585524"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235585524" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235585524">(Apr 21 2021 at 21:29)</a>:</h4>
<p>I understand what you're saying but I was talking in a more abstract way</p>



<a name="235585547"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235585547" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235585547">(Apr 21 2021 at 21:29)</a>:</h4>
<p>like it seems to me that this conceptually is saying</p>



<a name="235585609"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235585609" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235585609">(Apr 21 2021 at 21:30)</a>:</h4>
<p>in order to prove <code>LocalImplAllowed(Self: Trait&lt;P1...Pn&gt;)</code>, prove <code>LocalImplAllowed(Self: Trait&lt;P1...Pn&gt;)</code></p>



<a name="235585679"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235585679" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235585679">(Apr 21 2021 at 21:30)</a>:</h4>
<p>this is what I meant by ... I was expecting something that looks more like a leaf and not to see <code>LocalImplAllowed(Self: Trait&lt;P1...Pn&gt;)</code> as a fact</p>



<a name="235585759"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235585759" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235585759">(Apr 21 2021 at 21:31)</a>:</h4>
<p>Ah so</p>



<a name="235585790"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235585790" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235585790">(Apr 21 2021 at 21:31)</a>:</h4>
<p>I mean</p>



<a name="235585804"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235585804" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235585804">(Apr 21 2021 at 21:31)</a>:</h4>
<p>Hmm, trying to think of the best way to approach this</p>



<a name="235585863"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235585863" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235585863">(Apr 21 2021 at 21:32)</a>:</h4>
<p>So, let's think a bit more abstractly</p>



<a name="235585893"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235585893" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235585893">(Apr 21 2021 at 21:32)</a>:</h4>
<p>Imagine you had a goal <code>Implemented(T: Foo&lt;Bar&gt;)</code></p>



<a name="235585916"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235585916" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235585916">(Apr 21 2021 at 21:32)</a>:</h4>
<p>You could have a clause like <code>Implemented(T: Foo&lt;Bar&gt;)</code></p>



<a name="235585930"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235585930" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235585930">(Apr 21 2021 at 21:32)</a>:</h4>
<p>And that makes sense right?</p>



<a name="235585948"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235585948" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235585948">(Apr 21 2021 at 21:33)</a>:</h4>
<p><span aria-label="+1" class="emoji emoji-1f44d" role="img" title="+1">:+1:</span></p>



<a name="235586007"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235586007" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235586007">(Apr 21 2021 at 21:33)</a>:</h4>
<p><em>but</em>, you could also have a clause like <code>forall&lt;U&gt; { Implemented(T: Foo&lt;U&gt;) }</code></p>



<a name="235586010"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235586010" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235586010">(Apr 21 2021 at 21:33)</a>:</h4>
<p>I see what you mean yeah</p>



<a name="235586018"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235586018" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235586018">(Apr 21 2021 at 21:33)</a>:</h4>
<p>And that makes sense</p>



<a name="235586030"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235586030" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235586030">(Apr 21 2021 at 21:33)</a>:</h4>
<p><em>but</em> you can <em>also</em> have:</p>



<a name="235586057"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235586057" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235586057">(Apr 21 2021 at 21:33)</a>:</h4>
<p><code>Implemented(T: Foo&lt;Bar&gt;) :- Implemented(Bar: Baz)</code></p>



<a name="235586066"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235586066" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235586066">(Apr 21 2021 at 21:33)</a>:</h4>
<p>yep</p>



<a name="235586070"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235586070" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235586070">(Apr 21 2021 at 21:33)</a>:</h4>
<p>I see :)</p>



<a name="235586073"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235586073" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235586073">(Apr 21 2021 at 21:34)</a>:</h4>
<p>So, it</p>



<a name="235586114"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235586114" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Santiago Pastorino <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235586114">(Apr 21 2021 at 21:34)</a>:</h4>
<p><span aria-label="+1" class="emoji emoji-1f44d" role="img" title="+1">:+1:</span></p>



<a name="235586181"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235586181" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235586181">(Apr 21 2021 at 21:34)</a>:</h4>
<p>It's not super surprising that you see the goal as "just fact"</p>



<a name="235586229"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235586229" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235586229">(Apr 21 2021 at 21:35)</a>:</h4>
<p>And to continue just a bit more</p>



<a name="235586287"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235586287" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235586287">(Apr 21 2021 at 21:35)</a>:</h4>
<p>This sort of highlights that the clauses we generate are sort of separate from how we <em>use</em> them to solve our goal</p>



<a name="235586378"></a>
<h4><a href="https://rust-lang.zulipchat.com#narrow/stream/144729-wg-traits/topic/Chalk%20book%20modeling%20orphan%20check/near/235586378" class="zl"><img src="https://rust-lang.github.io/zulip_archive/assets/img/zulip.svg" alt="view this post on Zulip" style="width:20px;height:20px;"></a> Jack Huey <a href="https://rust-lang.github.io/zulip_archive/stream/144729-wg-traits/topic/Chalk.20book.20modeling.20orphan.20check.html#235586378">(Apr 21 2021 at 21:36)</a>:</h4>
<p>It's up to the solver to see that this provides a solution to that goal, exactly</p>



<hr><p>Last updated: Aug 07 2021 at 22:04 UTC</p>
</html>